\begin{tabbing}
$\forall$\=$i$:Id, ${\it ds}$:$x$:Id fp$\rightarrow$ Type, ${\it da}$:$k$:Knd fp$\rightarrow$ Type, $x$:Id, $T$:Type, $v$:$T$, ${\it ks}$:(Knd List),\+
\\[0ex]${\it tr}$:($k$:\{$k$:Knd$\mid$ ($k$ $\in$ ${\it ks}$)\} $\rightarrow$State(${\it ds}$)$\rightarrow$Valtype(${\it da}$;$k$)$\rightarrow$$T$$\rightarrow$$T$).
\-\\[0ex]($\neg$($\uparrow$$x$ $\in$ dom(${\it ds}$)))
\\[0ex]$\Rightarrow$ \=($\forall$$A$:Realizer.\+
\\[0ex]R{-}Feasible($A$)
\\[0ex]$\Rightarrow$ ($\neg$($\uparrow$R{-}occurs($A$;$i$;$x$)))
\\[0ex]$\Rightarrow$ ${\it ds}$ $\parallel$ R{-}ds($A$;$i$)
\\[0ex]$\Rightarrow$ ${\it da}$ $\parallel$ R{-}da($A$;$i$)
\\[0ex]$\Rightarrow$ ($\forall$$k$$\in$${\it ks}$. ($\uparrow$isrcv($k$)) $\Rightarrow$ (R{-}da($A$;source(lnk($k$)))($k$)?Void $\subseteq$r Valtype(${\it da}$;$k$)))
\\[0ex]$\Rightarrow$ ($\forall$$k$$\in$${\it ks}$. $\uparrow$$k$ $\in$ dom(${\it da}$))
\\[0ex]$\Rightarrow$ ($\forall$$k$:Knd. ($k$ $\in$ ${\it ks}$) $\Rightarrow$ ($\neg$($\uparrow$write{-}restricted($A$;$i$;$k$))))
\\[0ex]$\Rightarrow$ ($\forall$$y$:Id. ($\uparrow$$y$ $\in$ dom(${\it ds}$ $\oplus$ $x$ : $T$)) $\Rightarrow$ ($\neg$($\uparrow$read{-}restricted($A$; $i$; $y$))))
\\[0ex]$\Rightarrow$ R{-}state{-}var{-}init($i$;${\it ds}$;${\it da}$;$x$;$T$;$v$;${\it ks}$;${\it tr}$) $\parallel$ $A$)
\-
\end{tabbing}